Event B is a modelling language which can describe state-based models and required safety properties. The main objective is to provide a technique for incremental and proof-based development of the reactive systems. It integrates set-theoretical notations and a first-order predicate calculus, models called machines; it includes the concept of refinement expressing the simulation of machine by another one. An Event B machine models a reactive system i.e. a system driven by its environment and to its stimuli. An important property of these machines is that its events preserve the invariant properties defining a set of reachable states. The Evenet B method has been developed from the classical B method and it offers a general framework for developing the correct by construction systems by using an incremental approach for designing the models by refinement. Refinement is a relationship relating two models such that one model is simulating the other one. Refinement is also called refinement and preserves properties of the abstract model in the refined or concrete model. When an abstract model is refined by a concrete model, it means that the concrete model simulates the abstract model and that any safety property of the abstract model is also a safety property of the concrete model. In particular, the concrete model preserves the invariant properties of the abstract model. Event B aims to express models of systems characterized by its invariant and by a list of safety properties. However, we can consider liveness properties as in UNITY or TLA+ but in a restricted way.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001261 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001261 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:hal-00926335
   |texte=   Event B
}}